module sva_ca_repetition_1;

    logic clk;
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    logic a, b;
    initial begin
        a=1; b=1; #5;
        a=0; b=0; #10;
        a=1; b=0; #10;
        a=0; b=0; #10;
        a=0; b=1; #10;
        a=0; b=1; #10;
        a=0; b=1; #10;
        a=0; b=1; #10;
        a=0; b=1; #10;
        $finish;
    end

    // consecutive repetition: b[*3] 在功能上等价于 b ##1 b ##1 b
    // 含义: 如果信号 a 在时钟上升沿为真, 则从 2 个周期后开始, 信号 b 必须连续 3 个时钟周期为真.
    property p1;
        @(posedge clk) a |-> ##2 b[*3]; // a |-> ##2 b[*3] 等价于 a |-> ##2 (b ##1 b ##1 b);
    endproperty
    ap1: assert property(p1) $info("ap1 passed"); else $error("ap1 failed");

    // consecutive repetition: b[*2:4] 在功能上等价于 b[*2] or b[*3] or b[*4]
    // 含义: 如果信号 a 在时钟上升沿为真, 那么在两个时钟周期之后，信号 b 必须连续 3 ~ 5 个时钟周期为真.
    property p2;
        @(posedge clk) a |-> ##2 b[*2:4];
    endproperty
    ap2: assert property(p2) $info("ap2 passed"); else $error("ap2 failed");

    initial begin
        $dumpfile("dump.vcd"); $dumpvars;
    end
endmodule

/* Output: QuestaSim
# ** Error: ap2 failed
#    Time: 25 ns Started: 5 ns  Scope: sva_ca_repetition_1.ap2 File: sva_ca_repetition_1.sv Line: 35
# ** Error: ap1 failed
#    Time: 25 ns Started: 5 ns  Scope: sva_ca_repetition_1.ap1 File: sva_ca_repetition_1.sv Line: 28
# ** Info: ap2 passed
#    Time: 55 ns Started: 25 ns  Scope: sva_ca_repetition_1.ap2 File: sva_ca_repetition_1.sv Line: 35
# ** Info: ap1 passed
#    Time: 65 ns Started: 25 ns  Scope: sva_ca_repetition_1.ap1 File: sva_ca_repetition_1.sv Line: 28
 */